Nuprl Lemma : w-causl-time-iff
0,22
postcript
pdf
the_w
:World,
e
,
e'
:E. FairFifo
loc(
e
) = loc(
e'
)
Id
(
e
<c
e'
time(
e
)<time(
e'
))
latex
Definitions
e
<loc
e'
,
P
Q
,
e
<c
e'
,
time(
e
)
,
{
x
:
A
|
B
(
x
) }
,
,
Prop
,
loc(
e
)
,
FairFifo
,
E
,
World
,
a
<
b
,
s
=
t
,
Id
,
P
Q
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
:
A
B
(
x
)
,
t
T
,
P
&
Q
Lemmas
w-locl-iff
,
w-causl-time
,
world
wf
,
w-E
wf
,
fair-fifo
wf
,
w-loc
wf
,
Id
wf
,
nat
wf
,
w-time
wf
,
w-causl
wf
origin
the_w:World, e, e':E. FairFifo 
loc(e) = loc(e') 
Id (e <c e' 
time(e)<time(e')) the_w:World, e, e':E. FairFifo loc(e) = loc(e') Id (e <c e' time(e)<time(e')) Q
Q
B(x)x:A. B(x) Q
B(x) T